Nuprl Lemma : R-compat-Rplus-sq
11,40
postcript
pdf
A
,
B
,
C
:top.
sqequal(R-compat{i:l}(Rplus(
B
;
C
);
A
); (R-compat{i:l}(
B
;
A
)
R-compat{i:l}(
C
;
A
)))
latex
Definitions
t
T
,
tt
,
Rnone?(
x1
)
,
Rplus-right(
x1
)
,
Rplus-left(
x1
)
,
Rplus?(
x1
)
,
if
b
then
t
else
f
fi
,
Y
,
R-compat{i:l}(
A
;
B
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
A,B,C:top.
R-compat{i:l}(C; A))) A,B,C:top.
R-compat{i:l}(C; A))) 
Tx:A. B(x)